\begin{tabbing}
f{-}msg\=\{\$wanted:ut2, \$free:ut2, \$z:ut2\}\+
\\[0ex](${\it es}$; $L$; $e$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(es{-}loc(${\it es}$; $e$) $\in$ $L$ $\in$ Id)\+
\\[0ex]$\wedge$ \=(($\uparrow$es{-}isrcv(${\it es}$; $e$))\+
\\[0ex]c$\wedge$ \=(((es{-}tag(${\it es}$; $e$) = mkid\{\$wanted:ut2\} $\in$ Id)\+
\\[0ex]$\vee$ (es{-}tag(${\it es}$; $e$) = mkid\{\$free:ut2\} $\in$ Id))
\\[0ex]$\wedge$ ($\exists$\=$i$:Id\+
\\[0ex](($i$ $\in$ $L$ $\in$ Id)
\\[0ex]$\wedge$ ($\neg$($i$ = es{-}loc(${\it es}$; $e$) $\in$ Id))
\\[0ex]$\wedge$ (es{-}lnk(${\it es}$; $e$) = $<$$i$, es{-}loc(${\it es}$; $e$), mkid\{\$z:ut2\}$>$ $\in$ IdLnk)))))
\-\-\-\-
\end{tabbing}